00100	TITLE TD - TAUTOLOGY DETECTOR - BGB - 22 FEB 1973.
00200	
00300	SUBR(CMPILE)------------------------------------------------------
00400	BEGIN CMPILE; COMPILE POST FIX PROP. EXPR. - BGB - 22 FEB 73.
00500		Q←←16
00600		SETZM VARCNT
00700		LAC Q,[IOWD 2000,CODE]↔PUSH Q,[0]
00800	L0:	CALL(GETCHR)↔GO L3
00900	
01000	;OPERANDS - TRUTH TABLE PARALLEL BY WORD.
01100	
01200	L1:	CAIN"A"↔GO[PUSH Q,[PUSH P,[000000177777]]↔GO L0]
01300		CAIN"B"↔GO[PUSH Q,[PUSH P,[000077600377]]↔GO L0]
01400		CAIN"C"↔GO[PUSH Q,[PUSH P,[001703607417]]↔GO L0]
01500		CAIN"D"↔GO[PUSH Q,[PUSH P,[006314631463]]↔GO L0]
01600		CAIN"E"↔GO[PUSH Q,[PUSH P,[012525252525]]↔GO L0]
01700		CAIGE"F"↔GO L2↔CAILE"Z"↔GO L2
01800		ANDI 37↔CAMLE VARCNT↔DAC VARCNT
01900		ADD[PUSH P,VAR-6]↔PUSH Q,0↔GO L0
02000	
02100	;OPERATIONS.
02200	L2:
02300		CAIN"¬"↔GO[PUSH Q,[SETCMM(P)]↔GO L0]
02400		CAIN"∧"↔GO[PUSH Q,[POP P,]↔PUSH Q,[ANDM(P)]↔GO L0]
02500		CAIN"∨"↔GO[PUSH Q,[POP P,]↔PUSH Q,[IORM(P)]↔GO L0]
02600		CAIN"⊃"↔GO[PUSH Q,[POP P,]↔PUSH Q,[ORCAM(P)]↔GO L0]
02700		CAIN"⊗"↔GO[PUSH Q,[POP P,]↔PUSH Q,[XORM(P)]↔GO L0]
02800		CAIN"≡"↔GO[PUSH Q,[POP P,]↔PUSH Q,[EQVM(P)]↔GO L0]
02900		GO L0
03000	
03100	;END OF PARALLEL PASS.
03200	
03300	L3:	PUSH Q,[POP P,]
03400		PUSH Q,[CAME P,[IOWD PDLSIZ,PDL]]
03500		PUSH Q,[GO SHIT]
03600		PUSH Q,[SETCM]
03700		PUSH Q,[JUMPN FALSE]
03800		PUSH Q,[GO@CODE]
03900		POP0J
04000	
04100	FALSE: 	OUTSTR[ASCIZ/	NOT TAUTOLOGY./]↔GO SA
04200	SHIT: 	OUTSTR[ASCIZ/	NOT EXPRESSION./]↔GO SA
04300	
04400	BEND;2/22/73------------------------------------------------------
     

00100	SUBR(GETFIL)------------------------------------------------------
00200	BEGIN GETFIL; SETUP FILE SPEC FROM TTY LINE - BGB - 10 DEC 72.
00300	
00400		SETZM FILNAM↔SETZM EXTION↔SETZM EXTION+1↔SETZM PPPN
00500		OUTSTR[ASCIZ/	FILE = /]
00600		LAC 1,[POINT 6,FILNAM,-1]↔LACI 2,6
00700		INCHWL↔CAIL"a"↔SUBI 40
00800		CAIN 15↔GO[INCHWL↔POP0J]↔AOSA(P)
00900	
01000	L:	INCHWL↔CAIL"a"↔SUBI 40
01100		CAIN"."↔GO[LAC 1,[POINT 6,EXTION,-1]↔LACI 2,3↔GO L]
01200		CAIN"["↔GO[LAC 1,[POINT 6,PPPN,-1]  ↔LACI 2,3↔GO L]
01300		CAIN","↔GO[LAC 1,[POINT 6,PPPN,17]  ↔LACI 2,3↔GO L]
01400		CAIN"]"↔GO L
01500	
01600		CAIN 15↔GO EOL	;END OF THE LINE.
01700		CAIN 12↔GO EOL
01800		CAIG" "↔GO L	;IGNORE GARBAGE.
01900		SOJL 2,L
02000		SUBI 40↔IDPB 1↔GO L	;ASCII TO SIXBIT.
02100	
02200	EOL:	INCHWL↔CAR PPPN
02300		TRNN 77↔LSH -6↔TRNN 77↔LSH -6    ;RIGHT ADJUST PROJECT.
02400		DIP PPPN↔CDR PPPN
02500		TRNN 77↔LSH -6↔TRNN 77↔LSH -6    ;RIGHT ADJUST PROGRAMMER.
02600		DAP PPPN
02700		POP0J
02800	BEND;2/18/73-------------------------------------------------------
02900	
03000	SUBR(GETCHR)------------------------------------------------------
03100	BEGIN GETCHR; GET CHARACTER AND SKIP.
03200		SOSG IBUF+2↔IN 1,0
03300		GO[ILDB 0,IBUF+1↔AOS(P)↔POP0J]
03400		STATO 1,1B22↔GO[OUTSTR[ASCIZ/ INPUT ERROR./]↔HALT]
03500		POP0J
03600	BEND;2/22/73------------------------------------------------------
     

00100	;MAIN ENTRY.
00200		PDLSIZ←←450
00300	SA:	OUTSTR[BYTE(7)15,12]
00400		LAC P,[IOWD PDLSIZ,PDL]
00500		SETZM PDL↔LAC[XWD PDL,PDL+1]↔BLT PDL+177
00600		SKIPA
00700	
00800	;GET DISK FILE.
00900	L0:	RELEASE 1,↔CALL(GETFIL)↔CALLI 12
01000		INIT 1,0↔SIXBIT/DSK/↔IBUF↔HALT
01100		LOOKUP 1,FILNAM↔GO L0
01200		PUSH P,121↔LACI BUFFER↔DAC 121	;CREATE INPUT BUFFER.
01300		INBUF 1,↔POP P,121
01400	
01500	;COMPILE WFF EXPRESSION.
01600		CALL(CMPILE)
01700		SETZM VAR↔LAC[XWD VAR,VAR+1]↔BLT VAR+27	  ;CLEAR VARIABES.
01800		LAC VARCNT↔SUBI 5↔SKIPGE↔SETZ	;NUMBER BEYOND 5.
01900		LACI 1,1↔ROT 1,@0↔DAC 1,EXECNT	;NUMBER OF EXECUTIONS.
02000	
02100	;EXECUTE WFF CODE.
02200	L1:	SETZM PDL
02300		JSR CODE
02400		SOSG EXECNT↔GO L2
02500		LACI 1,VAR
02600		SETCMB(1)
02700		SKIPN↔AOJA 1,.-2
02800		GO L1
02900	L2:	OUTSTR[ASCIZ/	TAUTOLOGY./]↔GO SA
03000	
03100		LIT			;LITERALS.
03200		FILNAM:0		;FILE NAME.
03300		EXTION:0↔0		;EXTENSION.
03400		PPPN:0			;PROJECT-PROGRAMMER.
03500	
03600		IBUF:BLOCK 3		;INPUT BUFFER HEADER.
03700		EOF:0			;END OF FILE FLAG.
03800	
03900		VARCNT:0		;VARIABLE COUNT.
04000		EXECNT:0		;EXECUTIONS COUNT.
04100	
04200		PDL:BLOCK 40
04300		BUFFER:BLOCK 410	;INPUT BUFFER AND EXTRA PDL SPACE.
04400		VAR:BLOCK 30		;VARIABLES F THRU Z.
04500		CODE:BLOCK 2000		;COMPILE CODE.
04600	
04700	END SA